\begin{tabbing}
possible{-}world\=\{i:l\}\+
\\[0ex]($D$; $w$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=fair{-}fifo\=\{i:l\}\+\+
\\[0ex]($w$)
\-\\[0ex]\& (\=($\forall$$i$:Id, $x$:Id. w{-}vartype($w$; $i$; $x$) $\subseteq$r d{-}m($D$; $i$).ds($x$))\+
\\[0ex]c$\wedge$ \=($\forall$$i$:Id, $a$:w{-}action($w$; $i$).\+
\\[0ex]($\neg$($\uparrow$w{-}isnull($w$; $a$))) $\Rightarrow$ (w{-}valtype($w$; $i$; $a$) $\subseteq$r d{-}m($D$; $i$).da(w{-}kind($w$; $a$))))
\-\\[0ex]c$\wedge$ ($\forall$$l$:IdLnk, ${\it tg}$:Id. ($w$.M($l$,${\it tg}$)) $\subseteq$r d{-}m($D$; source($l$)).da(rcv($l$,${\it tg}$)))
\\[0ex]c$\wedge$ ($\forall$$i$:Id, $x$:Id. d{-}m($D$; $i$).init($x$,w{-}s($w$; $i$; 0; $x$)))
\\[0ex]c$\wedge$ \=($\forall$$i$:Id, $t$:$\mathbb{N}$.\+
\\[0ex]($\neg$($\uparrow$w{-}isnull($w$; w{-}a($w$; $i$; $t$))))
\\[0ex]$\Rightarrow$ \=((\=($\uparrow$islocal(w{-}kind($w$; w{-}a($w$; $i$; $t$))))\+\+
\\[0ex]$\Rightarrow$ \=(d{-}m($D$; $i$).pre(act(w{-}kind($w$; w{-}a($w$; $i$; $t$))),\+
\\[0ex]read{-}state($\lambda$$x$.w{-}s($w$; $i$; $t$; $x$)))
\\[0ex]\& ma{-}random(\=d{-}m($D$; $i$);\+
\\[0ex]w{-}valtype($w$; $i$; w{-}a($w$; $i$; $t$));
\\[0ex]w{-}val($w$; w{-}a($w$; $i$; $t$));
\\[0ex]$i$;
\\[0ex]act(w{-}kind($w$; w{-}a($w$; $i$; $t$)));
\\[0ex]w{-}knum($w$;$i$;w{-}kind($w$; w{-}a($w$; $i$; $t$));$t$))))
\-\-\-\\[0ex]\& (\=$\forall$$x$:Id.\+
\\[0ex]d{-}m($D$; $i$).ef(w{-}kind($w$; w{-}a($w$; $i$; $t$)),
\\[0ex]$x$,
\\[0ex]read{-}state($\lambda$$x$.w{-}s($w$; $i$; $t$; $x$)),
\\[0ex]w{-}val($w$; w{-}a($w$; $i$; $t$)),$\lambda$$q$.w{-}s($w$; $i$; ($t$+1); $x$)($q$ {-} 1)))
\-\\[0ex]\& (\=$\forall$$l$:IdLnk.\+
\\[0ex]d{-}m($D$; $i$).send(w{-}kind($w$; w{-}a($w$; $i$; $t$));
\\[0ex]$l$;
\\[0ex]read{-}state($\lambda$$x$.w{-}s($w$; $i$; $t$; $x$));
\\[0ex]w{-}val($w$; w{-}a($w$; $i$; $t$));withlnk($l$;w{-}m($w$; $i$; $t$));$i$))
\-\\[0ex]\& (\=$\forall$$x$:Id.\+
\\[0ex]($\neg$d{-}m($D$; $i$).frame(w{-}kind($w$; w{-}a($w$; $i$; $t$)) affects $x$))
\\[0ex]$\Rightarrow$ \=($\forall$$r$:$\mathbb{Q}$.\+
\\[0ex]w{-}s($w$; $i$; $t$; $x$)($r$ + 1) = w{-}s($w$; $i$; ($t$+1); $x$)($r$) $\in$ w{-}vartype($w$; $i$; $x$)))
\-\-\\[0ex]\& (\=$\forall$$l$:IdLnk, ${\it tg}$:Id.\+
\\[0ex]($\neg$d{-}m($D$; $i$).sframe(w{-}kind($w$; w{-}a($w$; $i$; $t$)) sends $<$$l$,${\it tg}$$>$))
\\[0ex]$\Rightarrow$ (w{-}tagged(${\it tg}$;onlnk($l$;w{-}m($w$; $i$; $t$))) = [] $\in$ (w{-}Msg($w$) List)))))
\-\-\-\\[0ex]c$\wedge$ \=((\=$\forall$$i$:Id, $a$:Id, $t$:$\mathbb{N}$.\+\+
\\[0ex]$\exists$\=${\it t'}$:$\mathbb{N}$\+
\\[0ex](($t$ $\leq$ ${\it t'}$)
\\[0ex]\& (\=(($\neg$($\uparrow$w{-}isnull($w$; w{-}a($w$; $i$; ${\it t'}$))))\+
\\[0ex]c$\wedge$ (w{-}kind($w$; w{-}a($w$; $i$; ${\it t'}$)) = locl($a$) $\in$ Knd))
\\[0ex]$\vee$ ($\neg$$a$ declared in d{-}m($D$; $i$))
\\[0ex]$\vee$ unsolvable d{-}m($D$; $i$).pre($a$,read{-}state($\lambda$$x$.w{-}s($w$; $i$; ${\it t'}$; $x$))))))
\-\-\-\\[0ex]\& (\=$\forall$$i$:Id, $t$:$\mathbb{N}$.\+
\\[0ex]($\neg$($\uparrow$w{-}isnull($w$; w{-}a($w$; $i$; $t$))))
\\[0ex]$\Rightarrow$ \=($\forall$$x$:Id.\+
\\[0ex]($\neg$d{-}m($D$; $i$).aframe(w{-}kind($w$; w{-}a($w$; $i$; $t$)) affects $x$))
\\[0ex]$\Rightarrow$ \=($\forall$$r$:$\mathbb{Q}$.\+
\\[0ex]w{-}s($w$; $i$; $t$; $x$)($r$ + 1)
\\[0ex]=
\\[0ex]w{-}s($w$; $i$; ($t$+1); $x$)($r$)
\\[0ex]$\in$ w{-}vartype($w$; $i$; $x$))))
\-\-\-\\[0ex]\& (\=$\forall$$i$:Id, $x$:Id, $k$:Knd.\+
\\[0ex]($\neg$d{-}m($D$; $i$).rframe($k$ reads $x$)) $\Rightarrow$ w{-}machine{-}independent($w$;$i$;$k$;$x$))
\-\\[0ex]\& (\=$\forall$$i$:Id, $t$:$\mathbb{N}$.\+
\\[0ex]($\neg$($\uparrow$w{-}isnull($w$; w{-}a($w$; $i$; $t$))))
\\[0ex]$\Rightarrow$ \=($\forall$$l$:IdLnk.\+
\\[0ex]($\neg$d{-}m($D$; $i$).bframe(w{-}kind($w$; w{-}a($w$; $i$; $t$)) sends on $l$))
\\[0ex]$\Rightarrow$ (onlnk($l$;w{-}m($w$; $i$; $t$)) = [] $\in$ (w{-}Msg($w$) List))))))
\-\-\-\-\-
\end{tabbing}